\begin{tabbing}
(\=(((((MoveToConcl ({-}1)) \+
\\[0ex]CollapseTHEN (GenConcl primrec($m$;$b$;$c$) = ${\it b'}$))$\cdot$) 
\\[0ex]CollapseTHEN (
\-\\[0ex](Auto\_aux (first\_nat 1:n) ((first\_nat 2:n),(first\_nat 3:n)) (first\_tok SupInf:t
\\[0ex])\= inil\_term)))$\cdot$) \+
\\[0ex]CollapseTHEN (Try ((ExtWith [`z'] [\{0..($n$+$m$)$^{-}$\}$\rightarrow$$T$$\rightarrow$$T$]) 
\\[0ex]CollapseTHEN (
\-\\[0ex](Auto\_aux (first\_nat 1:n) ((first\_nat 2:n),(first\_nat 3:n)) (first\_tok SupInf:t
\\[0ex]) inil\_term)))$\cdot$))$\cdot$
\end{tabbing}